i,a:Id, p:finite-prob-space, ds:fpf(Id; x.Type), P:(decl-state(ds)).
normal-ds{i:l}(ds)  R-realizes{i:l}(Rpre(i; ds; a; p; P); es.pre-p(es; i; ds; a; p; P)) 

latex

Definitions	x. t(x), t  T, R-Feasible{i:l}(R), P  Q, R-realizes{i:l}(R; es.P(es)), P  Q, x:A. B(x), x(s), R-consistent(R; es), prop{i:l}
Lemmas	finite-prob-space wf, Id wf, fpf wf, bool wf, decl-state wf, normal-ds wf, event system wf, Rpre wf, R-consistent wf